es-first-at-since(es;i;e;e.R(e);e.P(e))
== loc(e) = i & P(e) & R(e) & (e'<e. P(e')  (e'':E. e'  e''  & (e'' <loc e) & R(e''))) 

latex

---

clarification:

es-first-at-since(es;i;e;e.R(e);e.P(e))
== es-loc(es; e) = i  Id
== & P(e) & R(e)
== & alle-lt(es;e;e'.P(e')
== & alle-lt(es;e;e'. (e'':es-E(es). es-le(es;e';e'') & es-locl(es; e''; e) & R(e''))) 

latex

Definitions	es-first-at-since(es;i;e;e.R(e);e.P(e)), Id, loc(e), A, e<e'. P(e), P  Q, x:A. B(x), E, e  e' , P & Q, (e <loc e')
FDL editor aliases	es-first-at-since